ABS: Consistent(R;es)
STM: R-consistent wf
ABS: case(R)Rnone: noneleft right: comb(left;right)base(b). base(b)
STM: R-comb wf
right: comb(left;right)base(b). base(b) right: comb(left;right)base(b). base(b)